es:event_system{i:l}, L:(Id List).
fischer{x:ut2, try:ut2, taken:ut2, contending:ut2, free:ut2, mine:ut2, wanted:ut2, z:ut2}
fischer(es; L)
 prop{i:l} 

latex

Definitions	P  Q, x. t(x), False, A  B, IdLnk, x:A. B(x), P  Q, A, P  Q, P  Q, mkid{$x:ut2}, es-dtype(es; i; x; T), A c B, (x  l), P  Q, fischer, prop{i:l}, t  T, Id, x:A. B(x), x(s),
Lemmas	event system wf, Id wf, es-change-to wf, es-sender wf, es-loc wf, es-lnk wf, es-tag wf, iff wf, es-sends-on wf, false wf, l all wf2, es-when wf, es-initially wf, es-after wf, es-vartype wf, es-isconst wf, assert wf, select wf, length wf1, nat wf